Nuprl Definition : Q-R-pre-preserving 11,40

f is Q-R-pre-preserving on P == ee':{e:E| P(e)} . (Q(f(e),f(e')))  (R(e,e')) 
latex



clarification:

Q-R-pre-preserving(es;f;P;Q;R)
== e:{e:es-E(es)| P(e)} , e':{e:es-E(es)| P(e)} . (Q(f(e),f(e')))  (R(e,e')) 
latex


Definitionsx:AB(x), {x:AB(x)} , E, P  Q, f(a)
FDL editor aliasesQ-R-pre-preserving

origin